package controller;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;

import controller.preprocessor.PreProcessor;
import controller.preprocessor.PreProcessor;
import controller.preprocessor.ReViVal;
import controller.preprocessor.SatEllite1_0;
import controller.solver.Solver;
import controller.solver.MiniSat;
import controller.solver.RSat;
import controller.solver.Solver;

import model.BasicParameter;
import model.cnf.CNF;
import model.cnf.FileCNF;
import model.cnf.MemoryCNF;
import model.preprocessor.EPreProcessor;
import model.preprocessor.PreProcessorFactory;
import model.preprocessor.PreProcessorParameter;
import model.preprocessor.PreProcessorResult;
import model.solver.ESolver;
import model.solver.SolverFactory;
import model.solver.SolverParameter;
import model.solver.SolverResult;

public class Main {

	/**
	 * @param args
	 */
	public static void main(String[] args) {
		if(false)
			{
			debug();
			return;
			}
		else
			if(true)
			{
				run();
				return;
			}

		/*
		// TODO Auto-generated method stub
		InputStreamReader in = new InputStreamReader(System.in);
		BufferedReader input = new BufferedReader(in);
		
		
		try {
			System.out.println();
			System.out.println("------------Demarrage igsat------------");
			System.out.println();
			
			File dirpreproc = new File("preproc");
			File dirsolver = new File("solveur");
			File directoryNewCNF = new File("cnf");
			File directoryTstCNF = new File("tstcnf");
						
			if(dirpreproc.isDirectory())
				System.out.println("Dossier preproc recuperer : "+dirpreproc.getAbsolutePath());
			if(dirsolver.isDirectory())
				System.out.println("Dossier solver recuperer : "+dirsolver.getAbsolutePath());
			if(directoryNewCNF.isDirectory())
				System.out.println("Dossier pour nouvelle cnf recuperer : "+directoryNewCNF.getAbsolutePath());
			if(directoryTstCNF.isDirectory())
				System.out.println("Dossier de test par default cnf recuperer : "+directoryTstCNF.getAbsolutePath());

			boolean recommence;
			for(recommence = true ; recommence ; )
			{
				System.out.println();
				System.out.println("------------igsat------------");
				System.out.println();
				
				String cnf;
				while(true){
					System.out.println("Donner la CNF (ne pas utiliser de slash pour cherche dans ./tstcnf) : ");

					cnf = input.readLine();
					String ss ="";

					//System.out.println("first index : "+(cnf.indexOf('\\')-1));
					//retire "\ "
					if(cnf.indexOf('\\') != -1)
					{	  ss = cnf.substring(0, cnf.indexOf('\\')) + cnf.substring(cnf.indexOf('\\')+1);
					cnf = ss;
					}
					if(cnf.indexOf('/') == -1)
						cnf = directoryTstCNF.getAbsolutePath() + File.separatorChar + cnf + ".cnf";

					System.out.println("Chemin de la cnf = "+cnf);
					File f = new File(cnf);
					if(!f.isFile())
					{
						System.out.println("Le fichier n'existe pas");
						continue;
					}
					break;
				}
				
				boolean usesolver = false;
				while(true)
				{
					System.out.println("Utiliser prepocesseur ou solver ? : p/s");
					String rep = input.readLine();
					if(rep.equals(String.valueOf('p')))
					{
						usesolver = false;
						break;
					}
					if(rep.equals(String.valueOf('s')))
					{
						usesolver = true;
						break;
					}

				}

				PreProcessor preproc = null;
				Solver solver = null;
				boolean solutionSolveur = false;
				
				while(true)
				{//recupere l'instance
					if(usesolver)
					{//demande un solver
						System.out.println("Utiliser quel solveur : Minisat/rsat ? m/r");			
						String rep = input.readLine();
						
						if(rep.equals(String.valueOf('m')))
						{
							solver = new MiniSat(dirsolver);
							break;
						}
						if(rep.equals(String.valueOf('r')))
						{
							solver = new RSat(dirsolver);
							solutionSolveur = true;
							break;
						}
						
					}
					else
					{//demande preproc
						System.out.println("Utiliser quel prepocesseur : Revival/Satellite1.0 ? r/s");			
						String rep = input.readLine();
						
						if(rep.equals(String.valueOf('r')))
						{
							preproc = new ReViVal(dirpreproc);
							break;
						}
						if(rep.equals(String.valueOf('s')))
						{
							preproc = new SatEllite1_0(dirpreproc);
							break;
						}

					}

				}
				
				Integer timeout = null;
				while(true)
				{
					System.out.println("Utiliser timeout ? (en ms ; -1 = non ; 0 = default");
					String rep = input.readLine();
					
					timeout = Integer.parseInt(rep);
					
					if(timeout != null && timeout >= -1)
					{
						if(timeout == -1)
							timeout = BasicParameter.NO_DELAY;
					
						break;
					}
				}
				
				System.out.println();
				System.out.println("------------execution------------");
				System.out.println();
				System.out.print("Recupere CNF --> ");

				CNF filecnf = new FileCNF(cnf);
				if(filecnf == null)
				{
					System.out.println("FAIL -> quitte");
					return;
				}
				System.out.println("Fait");
				
				System.out.print("Cree parametre CNF --> ");

				if(usesolver){
					SolverParameter param = new SolverParameter();
					System.out.println("Fait");
						
					if(timeout != 0)
						param.setTimeOut(timeout);
					param.setPrintSolution(solutionSolveur);
					
					System.out.println("Run :");
					
					SolverResult res = solver.evaluate(filecnf, param); 

					System.out.println();
					System.out.println("------------fin de l'execution------------");
					System.out.println("------------Resultat------------");
					System.out.println();
					
					System.out.println(res.toString());
				}
				else
				{
					PreProcessorParameter param = new PreProcessorParameter("./cnf/newcnf.cnf");
					System.out.println("Fait");
					
					if(timeout != 0)
						param.setTimeOut(timeout);
					
					System.out.println();
					System.out.println("------------Run------------");
					System.out.println();
					
					PreProcessorResult res = preproc.evaluate(filecnf, param);

					System.out.println();
					System.out.println("------------fin de l'execution------------");
					System.out.println("------------Resultat------------");
					System.out.println();
					
					System.out.println(res.toString());	
				}
				
				while(true)
				{
					System.out.println();
					System.out.println("Recommencer ? : y/n");
					String rep = input.readLine();
					if(rep.equals(String.valueOf('y')))
					{
						recommence = true;
						break;
					}
					if(rep.equals(String.valueOf('n')))
					{
						recommence = false;
						break;
					}
				}
			}

		} catch (Exception e) {
			System.out.println("------------PROBLEM EXCEPTION RECUPERER -> QUIT------------");
			e.printStackTrace();
		}
	
		System.out.println("------------QUIT------------");*/
	}
	
	
	public static void run(){
		// TODO Auto-generated method stub
		InputStreamReader in = new InputStreamReader(System.in);
		BufferedReader input = new BufferedReader(in);
		
		
		try {
			System.out.println();
			System.out.println("------------Demarrage igsat------------");
			System.out.println();
			
			File dirpreproc = new File("preproc");
			File dirsolver = new File("solveur");
			File directoryNewCNF = new File("cnf");
			File directoryTstCNF = new File("tstcnf");
						
			if(dirpreproc.isDirectory())
				System.out.println("Dossier preproc recuperer : "+dirpreproc.getAbsolutePath());
			if(dirsolver.isDirectory())
				System.out.println("Dossier solver recuperer : "+dirsolver.getAbsolutePath());
			if(directoryNewCNF.isDirectory())
				System.out.println("Dossier pour nouvelle cnf recuperer : "+directoryNewCNF.getAbsolutePath());
			if(directoryTstCNF.isDirectory())
				System.out.println("Dossier de test par default cnf recuperer : "+directoryTstCNF.getAbsolutePath());

			boolean recommence;
			for(recommence = true ; recommence ; )
			{
				System.out.println();
				System.out.println("------------igsat------------");
				System.out.println();
				
				String cnf;
				while(true){
					System.out.println("Donner la CNF (ne pas utiliser de slash pour cherche dans ./tstcnf) : ");

					cnf = input.readLine();
					String ss ="";

					//System.out.println("first index : "+(cnf.indexOf('\\')-1));
					//retire "\ "
					if(cnf.indexOf('\\') != -1)
					{	  ss = cnf.substring(0, cnf.indexOf('\\')) + cnf.substring(cnf.indexOf('\\')+1);
					cnf = ss;
					}
					if(cnf.indexOf('/') == -1)
						cnf = directoryTstCNF.getAbsolutePath() + File.separatorChar + cnf + ".cnf";

					System.out.println("Chemin de la cnf = "+cnf);
					File f = new File(cnf);
					if(!f.isFile())
					{
						System.out.println("Le fichier n'existe pas");
						continue;
					}
					break;
				}
				
				boolean usesolver = false;
				while(true)
				{
					System.out.println("Utiliser prepocesseur ou solver ? : p/s");
					String rep = input.readLine();
					if(rep.equals(String.valueOf('p')))
					{
						usesolver = false;
						break;
					}
					if(rep.equals(String.valueOf('s')))
					{
						usesolver = true;
						break;
					}

				}

				SolverFactory solverfact = new SolverFactory(dirsolver);
				PreProcessorFactory preprocfact = new PreProcessorFactory(dirpreproc);
				PreProcessor preproc = null;
				Solver solver = null;
				//boolean solutionSolveur = false;
				
				while(true)
				{//recupere l'instance
					if(usesolver)
					{//demande un solver
						System.out.println("Utiliser quel solveur : Minisat/rsat ? m/r");			
						String rep = input.readLine();
						
						if(rep.equals(String.valueOf('m')))
						{
							solver = solverfact.createSolver(ESolver.MINISAT);
							break;
						}
						if(rep.equals(String.valueOf('r')))
						{
							solver = solverfact.createSolver(ESolver.RSAT);
							break;
						}
						
					}
					else
					{//demande preproc
						System.out.println("Utiliser quel prepocesseur : Revival/Satellite1.0/hypre ? r/s/h");			
						String rep = input.readLine();
						
						if(rep.equals(String.valueOf('r')))
						{
							preproc = preprocfact.createPreProcessor(EPreProcessor.REVIVAL);
							break;
						}
						if(rep.equals(String.valueOf('s')))
						{
							preproc = preprocfact.createPreProcessor(EPreProcessor.SATELLITE_1_0);
							break;
						}
						if(rep.equals(String.valueOf('h')))
						{
							preproc = preprocfact.createPreProcessor(EPreProcessor.HYPRE);
							break;
						}
						
					}

				}
				
				Integer timeout = null;
				while(true)
				{
					System.out.println("Utiliser timeout ? (en ms ; -1 = non ; 0 = default");
					String rep = input.readLine();
					
					timeout = Integer.parseInt(rep);
					
					if(timeout != null && timeout >= -1)
					{
						if(timeout == -1)
							timeout = BasicParameter.NO_DELAY;
						if(timeout == 0)
							timeout = BasicParameter.DEFAULT_DELAY;
					
						break;
					}
				}
				
				System.out.println();
				System.out.println("------------execution------------");
				System.out.println();
				System.out.print("Recupere CNF --> ");

				CNF filecnf = new FileCNF(cnf);
				if(filecnf == null)
				{
					System.out.println("FAIL -> quitte");
					return;
				}
				System.out.println("Fait");
				
				System.out.print("Add parametre CNF --> ");

				if(usesolver){
					System.out.println("Fait");
						
					solver.getSolverParameter().setTimeOut(timeout);
					//solver.setPrintSolution(true);
					
					System.out.println("Run :");
					
					SolverResult res = solver.evaluate(filecnf); 

					System.out.println();
					System.out.println("------------fin de l'execution------------");
					System.out.println("------------Resultat------------");
					System.out.println();
					
					System.out.println(res.toString());
				}
				else
				{
					preproc.getPreProcessorParameter().setOut("./cnf/newcnf.cnf");
					System.out.println("Fait");
					
					
					preproc.getPreProcessorParameter().setTimeOut(timeout);
					
					System.out.println();
					System.out.println("------------Run------------");
					System.out.println();
					
					PreProcessorResult res = preproc.evaluate(filecnf);

					System.out.println();
					System.out.println("------------fin de l'execution------------");
					System.out.println("------------Resultat------------");
					System.out.println();
					
					System.out.println(res.toString());	
				}
				
				while(true)
				{
					System.out.println();
					System.out.println("Recommencer ? : y/n");
					String rep = input.readLine();
					if(rep.equals(String.valueOf('y')))
					{
						recommence = true;
						break;
					}
					if(rep.equals(String.valueOf('n')))
					{
						recommence = false;
						break;
					}
				}
			}

		} catch (Exception e) {
			System.out.println("------------PROBLEM EXCEPTION RECUPERER -> QUIT------------");
			e.printStackTrace();
		}
	
		System.out.println("------------QUIT------------");
	}
	
	private static void debug(){
		File directoryTstCNF = new File("tstcnf");
		File cnf = new File(directoryTstCNF, "cour.cnf");
		
		MemoryCNF mem = null;
		try {
			mem = new MemoryCNF(cnf.getAbsolutePath());
			mem.checkStat();
		} catch (Exception e) {
			e.printStackTrace();
		} 
		
		System.out.println(mem.getStat());
		
		
	}

}
